Predicative Arithmetic by Edward Nelson

Predicative Arithmetic by Edward Nelson

Author:Edward Nelson
Language: eng
Format: epub
Tags: Arithmetic,


The ordinals are depicted on the vertical axis, and the portion of the figure lying strictly below the horizontal line through the ordinal a depicts the set R a of all sets of rank < a. Here i is the first inaccessible cardinal and m is the first measurable cardinal. The figure is not drawn to scale.

Figure 21.1: Cantor's Paradise

21. EXISTENCE OF SETS

97

Set theory is abstract, but abstract beliefs affect concrete actions. Someone who believes in R\ would consider it a waste of time to try to produce a contradiction from the axioms of ZFC; similarly for i2 w . 2 and Zermelo's original axiomatic set theory with separation but without replacement; and similarly for R^+i and Peano Arithmetic.

To a nominalist it is clear where to draw the line separating the real from the speculative: i2 5 , which is a system of 65536 objects, exists—but R e , with its 2 -ft 5 members, is only a formal construct.

Chapter 22

Semibounded replacement

This chapter is a digression, and I do not intend to use it in the sequel except in occasional remarks. The semibounded replacement principle differs from the bounded replacement principle of Chapter 17 in that 3yD is no longer required to be bounded, though D itself is.

Metatheorem 22.1 Let D be a bounded formula of Q\ such that Zi,..., x v art the variables distinct from x and y occurring free in D. Consider the formula

SBR. a is a set &: \fx{x Gfl-> 3yD) —-»

3f(f is a function & Dom / = a &; Vx(x € a —» D v [/(z)])).

Then Q' 4 '[(SBR)] is interpretable in Q\.

Demonstration. Let Di be min tf D. We want to construct the function / with domain a such that for x € a we have f(x) = y if and only if T>\. How do we know such a function exists? Write f[re] for

VaVxi • • • \fx v {a is a set & Card a < n Sl \fx{x tc-> 3yD) —>

3f{f is a function k. Dom / = a & Vx(x Eo-» Di)))-

We claim that ind n <;{n\. Clearly f[0]. Suppose

f[n] &; a is a set &; Card a = n-f 1 & Vx(a: € a —+ 3yD).

22. SEMIBOUNDED REPLACEMENT

99

There exists z such that 26 a. Let a 0 = {t € a : t ^ z}. Then there exists /o such that / 0 is a function & Dom / 0 = a 0 & Vxfx 6 a 0 -> Di). Since z G a we have Bit? D,„[zti;], so by BLNP there exists w such that Dije V [«u;]. Let / = / 0 U {(2,11;}}. Thus f[n] —► f[n + 1], and the claim is established.

Since £ is inductive, we can form f 4 and apply SREL of Chapter 15. Then we have f 4 [a] —► f 4 [Card a], and so f 4 [a] —► f[Carda], since Card is a bounded function symbol. Therefore we have

£ 4 [a] &; a is a set & Vx(x € a —► 3yD) —*

3/(/ is a function &: Dom/ = a & Vx(x 6 a —♦ Di))

and a fortiori

1.



Download



Copyright Disclaimer:
This site does not store any files on its server. We only index and link to content provided by other sites. Please contact the content providers to delete copyright contents if any and email us, we'll remove relevant links or contents immediately.